Nuprl Definition : ma-compatible-decls
0,22
postcript
pdf
M1
||decl
M2
== 1of(
M1
) || 1of(
M2
) & 1of(2of(
M1
)) || 1of(2of(
M2
))
latex
clarification:
ma-compatible-decls{i:l}
ma-compatible-decls
(
M1
;
M2
)
== fpf-compatible(Id;
x
.Type{i}; IdDeq; 1of(
M1
); 1of(
M2
))
==
& fpf-compatible(Knd;
x
.Type{i}; KindDeq; 1of(2of(
M1
)); 1of(2of(
M2
)))
latex
Definitions
P
&
Q
,
Id
,
IdDeq
,
f
||
g
,
Knd
,
Type
,
KindDeq
,
1of(
t
)
,
2of(
t
)
FDL editor aliases
ma-compatible-decls
origin